l:IdLnk, dt:tg:Id fp Type, a:Id. locl(a)  dom(lnk-decl(l;dt)) ~ false 

latex

Definitions	false, deq-member(eq;x;L), , t  T, {T}, P  Q, x:A. B(x), SQType(T), x  dom(f), lnk-decl(l;dt), a:A fp B(a), IdLnk, Id, x. t(x), False, P & Q, x:A. B(x), b, (x  l), Knd, rcv(l,tg), locl(a), P  Q, P  Q, map(f;as), KindDeq
Lemmas	not locl rcv, iff imp equal bool, deq-member wf, assert wf, bfalse wf, assert-deq-member, Kind-deq wf, map wf, member map, Knd wf, locl wf, rcv wf, fpf wf, Id wf, IdLnk wf, bool sq